COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	declare INDCONST T F ε Proposition
C00006 00003	axiom future:
C00009 00004	declare INDCONST Tm ε Thingconcept
C00010 ENDMK
C⊗;
declare INDCONST T F ε Proposition;
declare INDVAR Q Q0 Q1 Q2 Q3 Q4 ε Proposition;

DECLARE OPCONST And(Proposition,Proposition) = Proposition [L←655,R←650];
DECLARE OPCONST Or(Proposition,Proposition) = Proposition [L←635,R←640];
DECLARE OPCONST Implies(Proposition,Proposition) = Proposition [L←615,R←620];
DECLARE OPCONST Equiv(Proposition,Proposition) = Proposition [L←605,R←610];
DECLARE OPCONST Not(Proposition) = Proposition [R←675];

declare INDVAR X X0 X1 X2 X3 X4 ε Thingconcept;
declare INDVAR x x0 x1 x2 x3 x4 ε thing;
declare OPCONST Equal(Thingconcept,Thingconcept) = Proposition [L←685,R←690];
declare INDCONST world ε worlds;
declare INDVAR w w1 w2 w3 w4 ε worlds;

declare PREDCONST ttrue(Proposition) [R←600];
declare PREDCONST true(worlds,Proposition);
declare OPCONST Nec(Proposition) = Proposition [R←700];
declare PREDCONST nec(Proposition) [R←600];
declare PREDCONST prec(worlds,worlds) [inf];

declare OPCONST denot(worlds,Thingconcept) = thing;

declare INDCONST Mike Joe Pat ε Personconcept;
declare INDCONST mike joe pat ε person;
declare INDVAR P P1 P2 P3 P4 ε Personconcept;
declare INDVAR p p1 p2 p3 p4 ε person;

moregeneral Thingconcept ≥ {Personconcept};
moregeneral thing ≥ {person};

declare OPCONST Telephone(Personconcept) = Thingconcept[R←710];
declare OPCONST telephone(person) = thing [R←599];
axiom teldef:	∀P w.(denot(w,Telephone P) = telephone denot(w,P));;

declare OPCONST K(Personconcept,Proposition) = Proposition;
declare PREDCONST k(person,Proposition);

declare OPCONST Know(Personconcept,Thingconcept) = Proposition;
declare PREDCONST know(person,Thingconcept);

declare OPCONST Want(Personconcept,Proposition) = Proposition;
declare PREDCONST want(person,Proposition);

declare OPCONST Like(Personconcept,Personconcept) = Proposition;
declare PREDCONST like(person,Personconcept);

declare OPCONST Future(Proposition) = Proposition [R←695];
declare PREDCONST future(Proposition) [R←597];

declare INDVAR E E0 E1 E2 E3 E4 ε Eventconcept;
declare INDVAR A A0 A1 A2 A3 A4 ε Actionconcept;

declare OPCONST Cause(Eventconcept,Proposition) = Proposition;
declare OPCONST Do(Personconcept,Actionconcept) = Eventconcept;
declare OPCONST Occur(Eventconcept) = Proposition [R←695];
declare OPCONST Tell(Personconcept,Thingconcept) = Actionconcept;
axiom future:
	∀Q.nec(Q Implies Future Q)
	∀Q.nec(Future Future Q Implies Future Q)
	∀Q1 Q2.nec(Future Q1 And Nec Q2 Implies Future (Q1 And Q2))
	∀Q.(future Q ≡ true(world,Future Q))
	∀w Q.(true(w,Future Q) ≡ ∃w1.(w prec w1 ∧ true(w1,Q)))
;;

axiom logic:
	∀Q1 Q2 w.(true(w,Q1 And Q2) ≡ true(w,Q1) ∧ true(w,Q2))
	∀Q1 Q2 w.(true(w,Q1 Or Q2) ≡ true(w,Q1) ∨ true(w,Q2))
	∀Q1 Q2 w.(true(w,Q1 Implies Q2) ≡ true(w,Q1) ⊃ true(w,Q2))
	∀Q1 Q2 w.(true(w,Q1 Equiv Q2) ≡ (true(w,Q1) ≡ true(w,Q2)))
	∀Q w.(true(w,Not Q) ≡ ¬true(w,Q))
;;

axiom tell:
	∀P1 P2 X.(nec(Know(P1,X) Implies Cause(Do(P1,Tell(P2,X)),Know(P2,X))))
	∀P1 P2 Q.(nec(K(P1,Q) Implies Cause(Do(P1,Tell(P2,Q)),K(P2,Q))))
;;

axiom likewant:
	∀P1 P2 Q.nec(Like(P1,P2) And K(P1,Want(P2,Q)) Implies Want(P1,Q))
;;

axiom cause:
	∀E Q1 Q2.nec(Cause(E,Q1) And Cause(E,Q2) Implies Cause(E,Q1 And Q2))
	∀E Q.nec(Occur E And Cause(E,Q) Implies Future Q)
;;

axiom wantdo:
	∀P Q A.nec(Want(P,Q) And K(P,Occur Do(P,A) Implies Future Q)
Implies Occur Do(P,A))
;;

axiom nec:
	∀Q.(nec Q ≡ ∀w.true(w,Q))
	∀P Q.(nec Q ⊃ nec K(P,Q))
	∀Q1 Q2.(nec Q1 ∧ nec(Q1 Implies Q2) ⊃ nec Q2)
;;

axiom introspection:
	∀P X.nec(Know(P,X) Implies K(P,Know(P,X)))
	∀P Q.nec(K(P,Q) Implies K(P,K(P,Q)))
	∀P X.nec(Want(P,X) Implies K(P,Want(P,X)))
	∀P1 P2.nec(Like(P1,P2) Implies K(P1,Like(P1,P2)))
	∀P Q1 Q2.nec(K(P,Q1) And K(P,Q1 Implies Q2) Implies K(P,Q2))
;;

axiom world:
	∀Q.(ttrue Q ≡ true(world,Q))
;;
declare INDCONST Tm ε Thingconcept;
axiom problem1:
	ttrue Know(Pat,Tm)
	ttrue Want(Pat,Know(Joe,Tm))
;;